$\forall$$T$:Type. AtomFree(Type;$T$) $\Rightarrow$ ($\forall$$L$:$T$ List, $a$:Atom1. ($\exists$$x$:$T$. ($x$ $\in$ $L$) \& $x$:$T$$>>$$a$) $\Leftrightarrow$ $L$:$T$ List$>>$$a$)